credit2: Avoid extra c2t calcuation in csched_runtime

credit2: Avoid extra c2t calcuation in csched_runtime

csched_runtime() needs to call the ct2() function to change credits
into time.  The c2t() function, however, is expensive, as it requires
an integer division.

c2t() was being called twice, once for the main vcpu's credit and once
for the difference between its credit and the next in the queue.  But
this is unnecessary; by calculating in "credit" first, we can make it
so that we just do one conversion later in the algorithm.

This also adds more documentation describing the intended algorithm,
along with a relevant assertion..

The effect of the new code should be the same as the old code.

Spotted-by: Jan Beulich <JBeulich@suse.com>
Signed-off-by: George Dunlap <george.dunlap@eu.citrix.com>